\begin{tabbing}
$\forall$$D$:Dsys.
\\[0ex]($\forall$$l$:IdLnk, ${\it tg}$:Id. M(source($l$)).dout2($l$;${\it tg}$) $\subseteq$r M(destination($l$)).din($l$,${\it tg}$))
\\[0ex]$\Rightarrow$ \=(\=$\forall$$v$:($i$:Id$\rightarrow$M($i$).(timed)state), ${\it sched}$:(Id$\rightarrow$(?($\mathbb{N}\rightarrow$(IdLnk + Id)))),\+\+
\\[0ex]${\it dec}$:($i$,$a$:Id$\rightarrow\mathbb{N}\rightarrow$M($i$).state$\rightarrow$(?M($i$).da(locl($a$)))), $d$:(Id$\rightarrow$Id$\rightarrow\mathbb{B}$).
\-\\[0ex]d{-}comp($D$; $v$; ${\it sched}$; ${\it dec}$; $d$)
\\[0ex]$\in$ $t$:$\mathbb{N}\rightarrow$(\{0..$t$$^{-}$\}$\rightarrow$($i$:Id$\rightarrow$d{-}world{-}state($D$;$i$)))$\rightarrow$($i$:Id$\rightarrow$d{-}world{-}state($D$;$i$)))
\-
\end{tabbing}